a, b:. (a -- (a -- b)) = imin(a;b)   

latex

Up	int 2, int 2
Definitions	t  T, True, T, , a -- b, x:A. B(x), P  Q, P & Q, P  Q, P  Q, ff, tt, if b then t else f fi , imin(a;b), imax(a;b), , Unit, , False, A, A  B,
Lemmas	nat wf, imin wf, true wf, squash wf, imax wf, minus imax, add functionality wrt eq, add com, imin add r, assert of lt int, bnot of le int, eqff to assert, assert of le int, eqtt to assert, iff transitivity, imin com, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf